E, X1, X2:Type, info:(E(IdX1+(IdLnkE)X2)), pred?:(E(E+Unit)),
p:(e:E, l:IdLnk.
p:(e':E.
p:(e'':E.
p:(rcv?(e'')
p:( sender(e'') = e
p:( link(e'') = l
p:( e'' = e'  e'' < e' & loc(e') = destination(l)  Id), e:E, l:IdLnk.
sends-bound(p;e;l)  E 

latex

Definitions	Prop, Unit, sends-bound(p;e;l), x:A. B(x), 1of(t), x. t(x), b, rcv?(e), sender(e), IdLnk, link(e), P  Q, P & Q, P  Q, e < e', Id, loc(e), destination(l), x:A. B(x), t  T
Lemmas	ldst wf, loc wf, Id wf, cless wf, link wf, IdLnk wf, sender wf, rcv? wf, assert wf, pi1 wf, unit wf